Spec: limb decomposition discussion#669
Conversation
Codex Code ReviewFindings
No Rust/VM/security-relevant implementation changes are in this diff. I did not run a Typst build because |
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
Co-authored-by: claude[bot] <209825114+claude[bot]@users.noreply.github.com> Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>
|
The three points from Codex's review have been addressed in the previous commit (7111791) |
| :=(overline(w)_i + c_(i-1) - w_i ) dot L^(-1) | ||
| = floor.l (overline(w)_i + c_(i-1)) dot L^(-1) floor.r.$ | ||
| Hence, $c_i$ is maximized when both $overline(w)_i$ and $c_(i-1)$ are, and thus, | ||
| by induction, when $overline(w)_j$ is maximized for all $j in [0, i]$. |
There was a problem hiding this comment.
Technically the [0, i] should be [0, i), I suppose. Maybe just "for all i < j"
There was a problem hiding this comment.
Nope: [0, i]: c_i is defined in terms of overline(w)_i and thus, it is maximized when all overline(w)_j are for j <= i.
Also, i<j would be swapping the terms.
There was a problem hiding this comment.
Inclusion: yeah, fair
The second part was me swapping the operands accidentally, but I suppose the question then becomes whether j ≤ i is nicer to read that j ∈ [0, i]
| This includes $k = n-1$, which yields $c_(n+(n-1)) = c_(2n-1) <= mu - delta'$. | ||
| Moreover, $c_(2n) <= floor.l (mu - delta') dot L^(-1) floor.r = 0$ since $mu in [L]$ and thus $c_(2n + i) = 0$ for all $i >= 0$. | ||
| Applying this to @lm:wi_decomp_f, we conclude that $(w_0, w_1, ..., w_(2n-1), 0, 0, ...) in [L]^*$ is the unique limb decomposition | ||
| of $f_(alpha, mu) (x, y, z)$ when $mu = 0$ and $alpha < L$, or $mu = 1$ and $alpha <= 2$. |
There was a problem hiding this comment.
There bounds don't match the μ, α ∈ [L/2 - 1] from @lm:wi_decomp_f
|
|
||
| Now, observe that | ||
| $ | ||
| &max_(i in [2n]) min(mu (i+1) (L-1) + alpha - mu - delta, mu (2n-i-1)(L-2) + mu (2n-i) - delta')\ |
There was a problem hiding this comment.
I don't fully understand where this comes from, in particular the min.
I can see the 2n coming from n - (i - n), but somehow this assumes that the correct bound for one half is the minimum out of the two possible values, which is not a priori obvious.
e.g. for i = n - 1, we get min(μ n (L - 1) + α - μ - δ, μ n (L - 1) + μ - δ'), which would depend on the relation between μ and α, and for e.g. the case α = L/2 - 2, μ = 1 this would (wrongly) choose the second as upper bound.
Or in the degenerate case where μ = 0, we'd get min(α - 1, 0) = 0 everywhere as upper bound.
Probably the correct rephrasing is to take max(max_{i ∈ [n}(...), max_{k ∈ n}(...)) instead
| Note that the correctness of these constraints follows from @lm:limb-decomposition-constraint-correctness, when applied to $(S, L, C, alpha, mu) = (2^64, 2^32, 2, 2, 0)$: | ||
| - the definition of `carry` matches that of @eq:def_ci and @eq:c_-1_is_zero, | ||
| - @eq:range_ci is enforced by @add:c:carry, and | ||
| - @eq:range_wi follows from @add:a:sum. | ||
|
|
There was a problem hiding this comment.
I'm noticing that the labels of these references are broken; local referencing inside the limb-decomposition section is fine. Are you OK with using the equate package despite these broken labels?
There was a problem hiding this comment.
What exactly are we getting from equate? And does not using it fix the labels?
RobinJadoul
left a comment
RobinJadoul
left a comment
There was a problem hiding this comment.
A couple nits, some typography, and some weirdness left surrounding the corollary. But I think next pass should be there
| Note that the correctness of these constraints follows from @lm:limb-decomposition-constraint-correctness, when applied to $(S, L, C, alpha, mu) = (2^64, 2^32, 2, 2, 0)$: | ||
| - the definition of `carry` matches that of @eq:def_ci and @eq:c_-1_is_zero, | ||
| - @eq:range_ci is enforced by @add:c:carry, and | ||
| - @eq:range_wi follows from @add:a:sum. | ||
|
|
There was a problem hiding this comment.
What exactly are we getting from equate? And does not using it fix the labels?
| Let $[X]$ denote the set ${0, ..., X-1} subset.eq NN$. | ||
| Let $S := L^n in NN$ be an upper bound on the integers we want to represent, | ||
| where $L in NN without {0, 1}$ is the number of values a limb can represent | ||
| and $n in N$ denotes the number of limbs. |
There was a problem hiding this comment.
| and $n in N$ denotes the number of limbs. | |
| and $n in NN$ denotes the number of limbs. |
| where $L in NN without {0, 1}$ is the number of values a limb can represent | ||
| and $n in N$ denotes the number of limbs. | ||
|
|
||
| Observe that for all $x in [S]$, there exists a unique tuple of integers |
There was a problem hiding this comment.
| Observe that for all $x in [S]$, there exists a unique tuple of integers | |
| Observe that for all $x in [S]$, there exists a unique "limb decomposition" |
| = sum_(i=0)^(n-1) x_i dot L^i. | ||
| $ #<eq:decomposition> | ||
| To simplify future notation, we define $x_i := 0$ for all $i >= n$. | ||
| Next, we define the family of multi-linear functions |
There was a problem hiding this comment.
Do we care that the functions are multi-linear?
| To simplify future notation, we define $x_i := 0$ for all $i >= n$. | ||
| Next, we define the family of multi-linear functions | ||
| $ | ||
| f_(mu, alpha) (x, y, z) := sum_(m in [mu]) (x^((m)) dot y^((m))) + sum_(a in [alpha]) z^((a)) |
There was a problem hiding this comment.
Maybe make the variables boldface, as they're vectorial
| c_i <= &max(&max_(i in [n]) #h(1em) mu (i+1) (L-1) + alpha - mu - delta,\ | ||
| &max_(k in [n]) #h(1em) mu (2n-k-1)(L-2) + mu (2n-k) - delta')\ | ||
| &= max(& mu n (L-1) + alpha - mu - delta, mu (2n-1)(L-2) + 2 mu n - delta')\ | ||
| &= mu n (L-1) + alpha - mu - delta |
There was a problem hiding this comment.
Unless the 2s disappear, this doesn't hold, afaict; when they do disappear, it works (with L ≥ 2), except maybe some weirdness with the deltas I didn't work through entirely
| $ | ||
| ] | ||
|
|
||
| Note that this upper bound is tight: |
There was a problem hiding this comment.
How is this tight, if we're using the upper bound from the first half of the coefficients? Does this refer to the lemma 3 bound instead of the corollary?
| Note that this upper bound is tight: | ||
| $c_(n+k)$ achieves the bound for all $k in [n]$ when $x^((m)) = y^((m)) = z^((a)) = S-1$ for all $m in [mu]$ and $a in [alpha]$. | ||
| For $k = n-1$, this yields $c_(n+(n-1)) = c_(2n-1) <= mu - delta'$, which evaluates to zero when $mu = 0$ and $alpha < L$, or $mu = 1$ and $alpha <= 2$. | ||
| We can therefore conclude that $(w_0, w_1, ..., w_(2n-1)) in [L]^(2n)$ is a valid $2n$-limb decomposition of $f_(mu, alpha) (x, y, z)$ in these cases. |
There was a problem hiding this comment.
| We can therefore conclude that $(w_0, w_1, ..., w_(2n-1)) in [L]^(2n)$ is a valid $2n$-limb decomposition of $f_(mu, alpha) (x, y, z)$ in these cases. | |
| We can therefore conclude that $(w_0, w_1, ..., w_(2n-1)) in [L]^(2n)$ is a valid $2n$-limb decomposition of $f_(mu, alpha) (bold(x), bold(y), bold(z))$ in these cases. |
| where the utilized upper bound | ||
| $overline(w)_i <= mu n(L-1)^2 + alpha (L-1)$ | ||
| can be extracted from the proofs of @lm:carry-upperbound-pt1 and @lm:carry-upperbound-pt2. | ||
| Moreover, observe that $|X_i inter [L]| <= 1$ since $C < frac(p,L, style:"horizontal")$. |
There was a problem hiding this comment.
Maybe more clear as
| Moreover, observe that $|X_i inter [L]| <= 1$ since $C < frac(p,L, style:"horizontal")$. | |
| Moreover, observe that $|X_i inter [L]| <= 1$ since $0 <= C L < p$. |
| $ | ||
| where the utilized upper bound | ||
| $overline(w)_i <= mu n(L-1)^2 + alpha (L-1)$ | ||
| can be extracted from the proofs of @lm:carry-upperbound-pt1 and @lm:carry-upperbound-pt2. |
There was a problem hiding this comment.
Presumably we want to ref the corollary here, otherwise it's not doing much.
2 participants
This PR introduces a section that discusses (and proves) some properties of performing operations on limb decompositions.